/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ α≥EXPANDING THE ROLE OF VERIFICATION IN COMPUTER SCIENCE EDUCATION

␈↓ α∧␈↓␈↓ αTThe␈αfact␈αthat␈αcomputer␈αprograms␈αare␈αstill␈αdebugged␈αis␈αa␈αcontinuing␈αdisgrace␈αto␈αanyone␈αwho
␈↓ α∧␈↓thinks␈αmathematically.␈α The␈αway␈αof␈αgetting␈αa␈αprogram␈αcorrect␈αshould␈αbe␈αto␈αprove␈αthat␈αit␈αmeets␈αits
␈↓ α∧␈↓specifications␈α
and␈α∞check␈α
this␈α∞proof␈α
with␈α
a␈α∞computer.␈α
 As␈α∞much␈α
as␈α
possible,␈α∞the␈α
proof␈α∞should␈α
be
␈↓ α∧␈↓computer generated.

␈↓ α∧␈↓␈↓ αTOf␈α
course,␈α
this␈α
has␈αbeen␈α
the␈α
goal␈α
of␈α
program␈αverification␈α
research␈α
for␈α
many␈α
years,␈αand␈α
good
␈↓ α∧␈↓progress␈αhas␈αbeen␈αmade.␈α Even␈αthough␈αverification␈αhas␈αnot␈αprogressed␈αto␈αa␈αpoint␈αpermitting␈αlarge
␈↓ α∧␈↓practical␈αprograms␈αto␈αbe␈αverified␈αinstead␈αof␈αdebugged,␈αit␈αhas␈αreached␈αthe␈αpoint␈αwhere␈αstudents␈αin
␈↓ α∧␈↓programming courses will benefit from verifying many of the programs they write.

␈↓ α∧␈↓The␈α
benefits␈α
are␈α
twofold:␈α
First,␈α
a␈α
student␈α
who␈α
has␈α
verified␈α
a␈α
program␈α
understands␈α
what␈α
it␈αdoes
␈↓ α∧␈↓far␈α
better␈α
than␈α
one␈α
who␈α
has␈α
merely␈α
tinkered␈α∞with␈α
it␈α
till␈α
it␈α
works.␈α
 Second,␈α
if␈α
he␈α
must␈α∞verify␈α
his
␈↓ α∧␈↓programs,␈α
the␈α
student␈α
will␈αfind␈α
the␈α
exercise␈α
easier␈αif␈α
he␈α
makes␈α
a␈αwell␈α
structured␈α
prgram␈α
even␈αat
␈↓ α∧␈↓the␈α⊗cost␈α↔of␈α⊗rewriting␈α⊗it␈α↔as␈α⊗his␈α⊗understanding␈α↔improves.␈α⊗ For␈α⊗example,␈α↔none␈α⊗of␈α↔the␈α⊗bad
␈↓ α∧␈↓SAMEFRINGE␈α
programs␈α
published␈α
in␈α
the␈α
SIGART␈α
Newsletter␈α
last␈α
year␈α
would␈α
have␈α
survived␈α
an
␈↓ α∧␈↓attempt by the authors to verify them.

␈↓ α∧␈↓␈↓ αTIntroducing␈αverification␈αinto␈αthe␈α
teaching␈αof␈αprogramming␈αwill␈α
require␈αmuch␈αwork.␈α Here␈α
is
␈↓ α∧␈↓a plan for achieving it at Stanford:

␈↓ α∧␈↓␈↓ αT1.␈α∂Verification␈α∂should␈α∂be␈α∂separated␈α∂from␈α∂complexity␈α∂theory,␈α∂automata␈α∂theory␈α∂and␈α∞formal
␈↓ α∧␈↓language␈α∀theory␈α∀as␈α∀a␈α∀qualifying␈α∀exam␈α∀area␈α∀and␈α∀as␈α∀a␈α∀section␈α∀of␈α∀the␈α∀comprehensive␈α∪exam.
␈↓ α∧␈↓Verification␈α≡should␈α≥include␈α≡Hoare-type␈α≥methods,␈α≡verification␈α≥condition␈α≡generation,␈α≥the
␈↓ α∧␈↓Cartwright-McCarthy␈α↔method␈α↔of␈α↔expressing␈α↔LISP␈α↔programs␈α↔by␈α↔first␈α↔order␈α↔sentences␈α↔and
␈↓ α∧␈↓schemata, and the Scott formalisms.  A first step is the preparation of a qualifying exam syllabus.

␈↓ α∧␈↓␈↓ αT2.␈α⊂A␈α∂subset␈α⊂of␈α⊂this␈α∂should␈α⊂be␈α⊂on␈α∂the␈α⊂comprehensive␈α⊂syllabus.␈α∂ This␈α⊂should␈α⊂include␈α∂and
␈↓ α∧␈↓might␈α
be␈α
limited␈α
to␈α
the␈α
material␈α
on␈α
invariants␈α
in␈α
Manna's␈α
book␈α
and␈α
the␈α
material␈α
on␈α
first␈α
order
␈↓ α∧␈↓representation␈αin␈αthe␈αMcCarthy␈αand␈αTalcott␈αbook.␈α The␈αnecessary␈αbackground␈αin␈αfirst␈αorder␈αlogic
␈↓ α∧␈↓might be included in this part of the syllabus, especially since it is in the Manna book.

␈↓ α∧␈↓␈↓ αT3.␈α
The␈α∞programming␈α
problem␈α∞on␈α
the␈α
Comprehensive␈α∞should␈α
require␈α∞that␈α
the␈α∞program␈α
be
␈↓ α∧␈↓verified.␈α Given␈αthe␈αpresent␈αstate␈αof␈α
verification,␈αthis␈αwould␈αprobably␈αrequire␈αmaking␈αit␈α
somewhat
␈↓ α∧␈↓less␈α
ambitious␈α
as␈αa␈α
programming␈α
problem,␈αbut␈α
this␈α
part␈αof␈α
the␈α
exam␈αhas␈α
already␈α
received␈αmuch
␈↓ α∧␈↓criticism␈αas␈α
not␈αa␈α
scientific␈αexercise.␈α This␈α
cannot␈αbe␈α
done␈αuntil␈αthe␈α
one␈αor␈α
another␈αof␈αthe␈α
machine
␈↓ α∧␈↓verification systems has been made available for general use.

␈↓ α∧␈↓␈↓ αT4.␈α
The␈α
LISP␈α
course,␈α
now␈α
206,␈α
and␈α
soon␈α
to␈α
be␈α
126,␈α
should␈α
require␈α
machine␈α
verification␈αof
␈↓ α∧␈↓some␈α∞of␈α∞its␈α
programs,␈α∞perhaps␈α∞all␈α∞pure␈α
LISP␈α∞programs.␈α∞ This␈α
requires␈α∞the␈α∞implementation␈α∞of␈α
a
␈↓ α∧␈↓predicate␈α⊃calculus␈α⊃proof-checker␈α⊃as␈α⊃a␈α⊃feature␈α⊃of␈α⊃the␈α⊃student␈α⊃Maclisp␈α⊃system.␈α⊃ Making␈α⊃such␈α⊂a
␈↓ α∧␈↓system will be a major task, and we should get NSF to support a project aimed at this goal.

␈↓ α∧␈↓␈↓ αT5.␈α∃CS105␈α∃and␈α∃106␈α∃should␈α∃contain␈α∃some␈α∃verification.␈α∃ The␈α∃goal␈α∃of␈α⊗a␈α∃machine-aided
␈↓ α∧␈↓verification␈αsystem␈αfor␈αthese␈αcourses␈αis␈αvaguer␈αin␈αmy␈αmind,␈αand␈αtherefore␈αto␈αme␈αseems␈αfurther␈αoff.
␈↓ α∧␈↓However,␈α∂perhaps␈α∂the␈α⊂PASCAL␈α∂enthusiasts␈α∂would␈α∂think␈α⊂otherwise␈α∂and␈α∂would␈α∂be␈α⊂prepared␈α∂to
␈↓ α∧␈↓undertake␈α∞to␈α∞produce␈α∞a␈α∞PASCAL␈α∞verification␈α∞system␈α∞that␈α∞could␈α∞be␈α∞used␈α∞in␈α∂elementary␈α∞courses.
␈↓ α∧␈↓Most likely such a project would also require outside support.
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓␈↓ αT6.␈αIt␈αis␈αpossible␈αthat␈αlarge␈αamounts␈αof␈αstudent␈αverification␈αwill␈αincrease␈αour␈αcomputer␈αpower
␈↓ α∧␈↓requirements.

␈↓ α∧␈↓␈↓ αTStanford␈α
has␈α∞strong␈α
enough␈α∞faculty␈α
interests␈α∞in␈α
verification␈α∞including␈α
Floyd␈α∞(not␈α
presently
␈↓ α∧␈↓active␈α⊂here),␈α⊂Luckham,␈α⊂Manna,␈α⊂McCarthy,␈α⊂and␈α⊂Owicki,␈α⊃so␈α⊂that␈α⊂we␈α⊂are␈α⊂in␈α⊂a␈α⊂good␈α⊃position␈α⊂to
␈↓ α∧␈↓initiate the effort.  Weyhrauch, Talcott and Karp strengthen this effort.

␈↓ α∧␈↓␈↓ αTA␈α∞large␈α∞project␈α∂supported␈α∞by␈α∞the␈α∞education␈α∂part␈α∞of␈α∞NSF␈α∞aimed␈α∂at␈α∞making␈α∞it␈α∂practical␈α∞to
␈↓ α∧␈↓include verification in programming courses might be a good form of organization.